$\forall$$T$, ${\it T'}$:Type, $a$:($T$ List), $x$:${\it T'}$, $f$:(\{$x$:$T$$\mid$ ($x$ $\in$ $a$)\} $\rightarrow$${\it T'}$).
\\[0ex]($x$ $\in$ map($f$;$a$)) $\Leftarrow\!\Rightarrow$ ($\exists$$y$:$T$. (($y$ $\in$ $a$) \& $x$ = $f$($y$)))